Search for: All records

Hamiltonian simulation is a central application of quantum computing, with significant potential in modeling physical systems and solving complex optimization problems. Existing compilers for such simulations typically focus on low-level representations based on Pauli operators, limiting programmability and offering no formal guarantees of correctness across the compilation pipeline. We introduce QBlue, a high-level, formally verified framework for compiling Hamiltonian simulations. QBlue is based on the formalism of second quantization, which provides a natural and expressive way to describe quantum particle systems using creation and annihilation operators. To ensure safety and correctness, QBlue includes a type system that tracks particle types and enforces Hermitian structure. The framework supports compilation to both digital and analog quantum circuits and captures multiple layers of semantics, from static constraints to dynamic evolution. All components of QBlue, including its language design, type system, and compilation correctness, are fully mechanized in the Rocq proof framework, making it the first end-to-end verified compiler for second-quantized Hamiltonian simulation. 

Optical photothermal infrared spectroscopy (O-PTIR) was used to characterize a terrestrial rock sample as a demonstration of the technique’s enhanced spatial resolution as it corresponds to minerology and the detection of organics. Traditional reflectance-based infrared techniques are limited by the wavelength of the infrared light interacting with the surface along with additional optical dispersion issues. However, because of the nature in which the infrared spectrum is measured via O-PTIR, these traditional issues are eliminated. This is possible through the recent developments of high intensity quantum cascade-based infrared lasers capable of scanning the mid infrared spectrum (3000–500 cm−1). Individual O-PTIR and diffuse reflectance data were collected on a terrestrial rock sample and compared to a recent discovery of NASA JPL’s Perseverance Rover regarding inclusions of comparable size. In addition, an O-PTIR map of a particularly dense area of proteinaceous material in the terrestrial sample was collected, further exemplifying the capability. This technique has significant potential for use regarding future returned Mars samples and in situ planetary surface science when considering the spatial resolution, sensitivity, and negligible sample preparation. 

Large-amplitude variations are commonly observed in the atmospheres of directly imaged exoplanets and brown dwarfs. VHS 1256B, the most variable known planet-mass object, exhibits a near-infrared flux change of nearly 40%, with red color and silicate features revealed in recent JWST spectra, challenging current theories. Using a general circulation model, we demonstrate that VHS 1256B’s atmosphere is dominated by planetary-scale dust storms persisting for tens of days, with large patchy clouds propagating with equatorial waves. This weather pattern, distinct from the banded structures seen on solar system giants, simultaneously explains the observed spectra and critical features in the rotational light curves, including the large amplitude, irregular evolution, and wavelength dependence, as well as the variability trends observed in near-infrared color-magnitude diagrams of dusty substellar atmospheres. 

We measured carbon dioxide and methane flux exchange with the atmosphere at the deepest site of Falling Creek Reservoir (Vinton, Virginia, USA) every 30 minutes from 04 April 2020 to 31 December 2024. Falling Creek Reservoir is a drinking water supply reservoir owned and managed by the Western Virginia Water Authority (WVWA) as a primary drinking water source. The dataset consists of micrometeorological and flux data collected using an eddy covariance system (LiCor Biosciences, Lincoln, Nebraska, USA) and analyzed with associated Eddy Pro software (Eddy Pro Version 7.0.6), including carbon dioxide, methane, and water vapor. All analysis scripts are included for data processing and quality assurance/quality control following best practices.